abstract:

Security-critical applications constantly face threats from exploits in lower computing layers such as the OS and Hypervisor, or even attacks from malicious administrators. To protect sensitive data from such privileged adversaries, there is increasing development of secure hardware primitives, such as Intel SGX. Intel SGX instructions enable user mode applications to package trusted code and data into regions that are isolated from all other software on the machine, and also provide cryptographic primitives such as remote attestation. Our research is developing a principled approach to building cloud services with end-to-end security guarantees, including only these trusted hardware primitives in our trusted computing base. In this talk, I will demonstrate how one can use compiler and verification techniques to develop formally verified SGX programs, and demonstrate applications where Map-Reduce programs running on SGX can be certified to not leak secrets.

bio:

Rohit Sinha is currently pursuing a Ph.D. in EECS at UC Berkeley, where he works with Prof. Sanjit Seshia. His research interests include programming languages, software verification, and security.

Title:

Formally Verifying Implementations of Distributed Systems

Abstract:

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. In this talk, we'll survey the Verdi project which provides a framework for implementing and formally verifying implementations of distributed systems in Coq. Verdi eases the verification burden by enabling developers to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. Using this approach, the Verdi team produced the first correctness proof for an implementation of the Raft distributed consensus protocol.

Bio:

Zach Tatlock is an Assistant Professor in Computer Science and Engineering at the University of Washington where he leads the Programming Languages and Software Engineering (PLSE) group. He received his PhD from UC San Diego and BS from Purdue (where he took nearly every course with Bill Harris!). His research draws upon proof assistants, SMT solvers, and type systems to improve software reliability and security in domains ranging from distributed systems and compilers to web browsers. He can juggle and solve Rubik’s cubes, but not at the same time.